\section{Example of derivation}

This example show the derivation of the type of a  process that involves a complicate pattern for delegation: i.e. the execution of a session starts in process $P_1$, it is then delegated to process $P_2$ which executes one part and then returns it back to process $P_1$ that terminates the communication.

We consider the process $P_1 \parallel P_2 \parallel P_3$ where
$$
\begin{array}{ll}
 P_1 ::= &  \nopen{a}{c:{\sigma_1}}.\outC{c}{v}.\nopen{b}{d:\sigma_2}.\throw{d}{c}.\catch{d}{x}.\close{d}.\outC{x}{v}.\close{x}.\\
P_2::= & \nopen{b}{d:\overline{\sigma_2}}.\catch{d}{x}.\inC{x}{y}.\throw{d}{x}.\close{d} \\
P_3::=  & \nopen{a}{c:\overline{\sigma_1}}.\inC{c}{x}.\outC{c}{v}.\inC{c}{x}.\close{c}
\end{array}
$$
and $\sigma_1 = \tout{\capab}.\tin{\capab}.\tout{\capab}.\epsilon$ and $\sigma_2 = \tout{\tin{\capab}.\tout{\capab}.\epsilon}.\tin{ \tout{\capab}.\epsilon}.\epsilon$.

We now derive the type of $P_1$

$$
\infer[\rulenames{t:Open}]
{\judgebis{\env{\emptyset}{\emptyset}}{ P_1}{\type{\emptyset}{\{\sigma_1, \sigma_2 \} }}}
{\infer[\rulenames{t:Out}]
{\judgebis{\env{\emptyset}{\emptyset}}{ \outC{c}{v}.\nopen{b}{d:\sigma_2}.\throw{d}{c}.\catch{d}{x}.\close{d}.\outC{x}{v}.\close{x}}{\type{c:\sigma_1}{\{ \sigma_2 \} }}}
{\emptyset \vdash v:\capab & 
\infer[\rulenames{t:Open}]
{\judgebis{\env{\emptyset}{\emptyset}}{ \nopen{b}{d:\sigma_2}.\throw{d}{c}.\catch{d}{x}.\close{d}.\outC{x}{v}.\close{x}}{\type{c:\tin{\capab}.\tout{\capab}.\epsilon}{\{ \sigma_2 \} }}}
{\infer[\rulenames{t:Thr}]
{\judgebis{\env{\emptyset}{\emptyset}}{\throw{d}{c}.\catch{d}{x}.\close{d}.\outC{x}{v}.\close{x}}{\type{c:\tin{\capab}.\tout{\capab}.\epsilon, d: \sigma_2}{\emptyset }}}
{\infer[\rulenames{t:Cat}]
{\judgebis{\env{\emptyset}{\emptyset}}{\catch{d}{x}.\close{d}.\outC{x}{v}.\close{x}}{\type{ d: \tin{ \tout{\capab}.\epsilon}.\epsilon}{\emptyset }}}
{\infer[\rulenames{t:Clo}]
{\judgebis{\env{\emptyset}{\emptyset}}{\close{d}.\outC{x}{v}.\close{x}}{\type{ d: \epsilon, x:\tout{\capab}.\epsilon}{\emptyset }}}
{\infer[\rulenames{t:Out}]
{\judgebis{\env{\emptyset}{\emptyset}}{\outC{x}{v}.\close{x}}{\type{ x:\tout{\capab}.\epsilon}{\emptyset }}}
{\emptyset \vdash v:\capab &
 \infer[\rulenames{t:Clo}]
{\judgebis{\env{\emptyset}{\emptyset}}{\close{x}}{\type{ x:\epsilon}{\emptyset }}}
{\judgebis{\env{\emptyset}{\emptyset}}{\nil}{\type{ \emptyset}{\emptyset }}
}
}
}
}
}
}
}
}
$$
and the type of $P_2$
$$
\infer[\rulenames{t:Open}]
{\judgebis{\env{\emptyset}{\emptyset}}{ P_2}{\type{\emptyset}{\{\overline{\sigma_2 } \}}}}
{\infer[\rulenames{t:Cat}]
{\judgebis{\env{\emptyset}{\emptyset}}{\catch{d}{x}.\inC{x}{y}.\throw{d}{x}.\close{d}}{\type{d:\overline{\sigma_2}}{\emptyset}}}
{\infer[\rulenames{t:In}]
{\judgebis{\env{\emptyset}{\emptyset}}{\inC{x}{y}.\throw{d}{x}.\close{d}}{\type{d:\tout{ \tout{\capab}.\epsilon}.\epsilon, x: \tin{\capab}.\tout{\capab}.\epsilon}{\emptyset}}}
{\infer[\rulenames{t:Thr}]
{\judgebis{\env{y:\capab}{\emptyset}}{\throw{d}{x}.\close{d}}{\type{d:\tout{ \tout{\capab}.\epsilon}.\epsilon, x:\tout{\capab}.\epsilon}{\emptyset}}}
{\infer[\rulenames{t:Clo}]
{\judgebis{\env{y:\capab}{\emptyset}}{\close{d}}{\type{d:\epsilon}{\emptyset}}}
{\judgebis{\env{y:\capab}{\emptyset}}{\nil}{\type{\emptyset}{\emptyset}}}
}
}
}
}
$$

